(*************************************************************************)
(** Simply-typed Scalina  in Coq.    Infrastructure                      *)
(** Author: Adriaan Moors, 2008                                          *)
(*************************************************************************)

(** Based on the Coq tutorial at POPL 2008, see
    "Engineering Formal Metatheory", Aydemir, Charguéraud, Pierce,
    Pollack, Weirich. POPL 2008.

    Tutorial authors: Brian Aydemir and Stephanie Weirich, with help
    from Aaron Bohannon, Nate Foster, Benjamin Pierce, Jeffrey
    Vaughan, Dimitrios Vytiniotis, and Steve Zdancewic.  Adapted from
    code by Arthur Charguéraud.
*)

Set Implicit Arguments.
Require Import Metatheory Scalina_Definitions support.
Require Import List.

(* from http://logical.futurs.inria.fr/cgi-bin/bugzilla/show_bug.cgi?id=1751#c1 *)

Definition list_f_ind (A: Set) (P : A -> Prop) (P' : list A -> Prop)
    (f:forall t, P t) (Hnil: P' nil) 
    (Hcons : forall T Ts, P T -> P' Ts -> P' (cons T Ts)) : forall l, P' l :=
 fix lf (l:list A) : P' l :=
   match l return P' l with 
   | nil => Hnil 
   | a::tl => Hcons _ _ (f a) (lf tl)
   end. 

(** Defining our own induction principle, as Coq does not consider subterms with types such as "option tp",
With the standard induction principle, we have to prove stuff about a `tp_struct optSelf mems` without 
knowing anything about optSelf and mems. With our more powerful induction principle, this case gets two
extra hypotheses:
  in case optSelf was Some t: P0 t and P1lst ms
  in case optSelf was None: P1lst ms

The user of the induction principle has to prove P1nil and P1cons below (inductively, these say that 
P1list holds for a list if P1 holds for every element of that list)

We use a section to avoid having to repeat all these variables.
*)
Section Induction.

(* variables will automatically be abstracted over where needed once section is closed (p. 32) *)
(* expanding the case for option tm and option tp inline, don't want to generate two more P's -- or would that be better? *)
Variables  (P : tm -> Prop) (P0 : tp -> Prop) (P1 : mem -> Prop) (P1lst : list mem -> Prop)
  (f : forall n : nat, P n)  (*case fvar*)
  (f0 : forall a : var, P a) (*case bvar *)
  (f1 : forall t : tm, P t -> forall l : lab, P (sel t l)) (*case sel*)
  (f2 : forall t : tp, P0 t -> P (new t))  (* case new t *)
  (f3n : forall (ms : list mem),  P1lst ms -> P0 (tp_struct None  ms))  (* case tp_struct None _ *)
  (f3s : forall (t : tp) (ms : list mem),  P0 t -> P1lst ms -> P0 (tp_struct (Some t) ms)) (* case tp_struct (Some t) _*)
  (f4n : forall (l : lab) (t : tp), P0 t -> P1 (mtm l t None))  (* case mtm _ _ None *)
  (f4s : forall (l : lab) (t : tp) (rhs: tm), P0 t -> P rhs -> P1 (mtm l t (Some rhs))) (* case mtm _ _ (Some rhs) *)
  (P1nil: P1lst nil) (* to relate P1 and P1lst, case for nil *)
  (P1cons : forall T Ts, P1 T -> P1lst Ts -> P1lst (cons T Ts)). (* to relate P1 and P1lst, case for cons *)

(* mostly the same as what Coq generates using 
Scheme tm_ind_3 := Induction for tm Sort Prop
  with tp_ind_3  := Induction for tp Sort Prop
  with mem_ind_3  := Induction for mem Sort Prop.

The important difference is that the last two induction principles also 
consider option's and list's of the inductive types
*)
Fixpoint my_tm_ind_3 (t : tm) : P t :=
  match t as t0 return (P t0) with
  | bvar n => f n
  | fvar a => f0 a
  | sel t0 l => f1 (my_tm_ind_3 t0) l
  | new t0 => f2 (my_tp_ind3 t0)
  end
with my_tp_ind3 (t : tp) : P0 t :=
  match t as t0 return (P0 t0) with
  | tp_struct None ms => f3n (list_f_ind P1 P1lst my_mem_ind3 P1nil P1cons ms)
  | tp_struct (Some t) ms => f3s (my_tp_ind3 t) (list_f_ind P1 P1lst my_mem_ind3 P1nil P1cons ms)
  end
with my_mem_ind3 (m : mem) : P1 m :=
  match m as m0 return (P1 m0) with
  | mtm l t None => f4n l (my_tp_ind3 t)
  | mtm l t (Some rhs) => f4s l (my_tp_ind3 t) (my_tm_ind_3 rhs)
  end.


Lemma tm_tp_mem_mutual_ind:
       (forall tm0 : tm, P tm0) /\  
       (forall tp0 : tp, P0 tp0) /\ 
       (forall mem0 : mem, P1 mem0) /\
       (forall mems : list mem, P1lst mems).
Proof.
 intros. split. apply (my_tm_ind_3); assumption.
 split. apply (my_tp_ind3); assumption.
 split. apply (my_mem_ind3); assumption.
 apply (list_f_ind P1 P1lst my_mem_ind3). auto. auto.
Qed.

End Induction.

Scheme lc_tm_ind_4 := Induction for lc_tm Sort Prop
  with lc_tp_ind_4  := Induction for lc_tp Sort Prop
  with lc_mem_ind_4  := Induction for lc_mem Sort Prop
  with lc_mems_ind_4  := Induction for lc_mems Sort Prop.
Combined Scheme lc_tm_tp_mem_mems_mutual_ind from lc_tm_ind_4, lc_tp_ind_4, lc_mem_ind_4, lc_mems_ind_4.


Scheme typing_ind_mi := Induction for typing Sort Prop
  with wf_tp_ind_mi := Induction for wf_tp Sort Prop
  with concrete_tp_ind_mi := Induction for concrete_tp Sort Prop
  with expand_ind_mi := Induction for expand Sort Prop
  with wf_env_ind_mi := Induction for wf_env Sort Prop
  with wf_mem_ind_mi := Induction for wf_mem Sort Prop
  with wf_mems_ind_mi := Induction for wf_mems Sort Prop.
Combined Scheme typing_wf_mutual_ind from typing_ind_mi, wf_tp_ind_mi, concrete_tp_ind_mi, expand_ind_mi, wf_env_ind_mi, wf_mem_ind_mi, wf_mems_ind_mi.
